% Created 2020-04-19 Sun 10:49
% Intended LaTeX compiler: pdflatex
\documentclass[presentation]{beamer}
                                  \usepackage{xeCJK}
\setCJKmainfont{Source Han Serif CN}
\setCJKmonofont{Source Han Serif CN}
\setmonofont{JetBrains Mono}
\usepackage[cache=false]{minted}
\usemintedstyle{rainbow_dash}
\usebackgroundtemplate{\includegraphics[width=\paperwidth,height=\paperheight]{../bg.jpg}}
\definecolor{BG_COLOR}{RGB}{1,137,255}
\setbeamercolor{frametitle}{bg=BG_COLOR}
\setminted{fontsize=\footnotesize}
\setbeamerfont{page number in head/foot}{size=\tiny}

                 \usepackage{default}
\usetheme[numbering=none]{metropolis}
\date{2020-04-18}
\title{Shapeless 入门指南}
\author{Jilen}
\subtitle{ 分享一些 shapleess 的一些学习经验 }
\institute[Dripower]{水滴技术团队\\\url{https://scala.cool}}
\hypersetup{
 pdfauthor={Jilen \href{mailto:jilen.zhang@gmail.com}{Jilen} \texorpdfstring\{Jilen\newline\url{jilen.zhang@gmail.com}\}\{Jilen\} \%},
 pdftitle={Shapeless 入门指南},
 pdfkeywords={},
 pdfsubject={},
 pdfcreator={Emacs 27.0.60 (Org mode 9.1.14)}, 
 pdflang={English}}
\begin{document}

\maketitle


\begin{frame}[label={sec:orgb84ef14}]{类型编程}
\begin{itemize}
\item Typeclass Derivation
\item Higher Rank Polymorphism
\end{itemize}
\end{frame}

\begin{frame}[fragile,label={sec:orga20bdbb}]{Higher Rank Polymorphism}
 \begin{minted}[]{scala}
import poly._

// choose is a function from Sets to Options with no type specific cases
object choose extends (Set ~> Option) {
  def apply[T](s : Set[T]) = s.headOption
}

scala> choose(Set(1, 2, 3))
res0: Option[Int] = Some(1)

scala> choose(Set('a', 'b', 'c'))
res1: Option[Char] = Some(a)
\end{minted}
\end{frame}

\begin{frame}[label={sec:orge5210d3}]{(Peano Encoding)}
一个集合 N = \{0, 1, 2, 3, \ldots{}\}

\begin{itemize}
\item 基本元素: 0，以及 ++ （后继关系）
\item 0 是自然数
\item 如果 n 是自然数，n++ 也是自然数
\end{itemize}
\end{frame}

\begin{frame}[fragile,label={sec:orgd4f29b1}]{自然数 (Scala Type System)}
 \begin{minted}[]{scala}
trait Nat {
  type N <: Nat
}

case class Succ[P <: Nat]() extends Nat {
  type N = Succ[P]
}

class _0 extends Nat with Serializable {
  type N = _0
}
\end{minted}
\end{frame}

\begin{frame}[label={sec:orgc00e18d}]{Peano Encoding 一些其他公理（一）}
\alert{0 不是任何数后继}

排除了 N = \{0, 1, 2, 3, 0\} 的情况
\end{frame}

\begin{frame}[label={sec:org6e6c1dc}]{Peano Encoding 一些其他公理（二）}
\alert{不同自然数后继不同}

排除了 N = \{0, 1, 2, 3\} 的情况
\end{frame}

\begin{frame}[fragile,label={sec:org45aeacc}]{Peano Encoding 一些其他公理（三-一）}
 \alert{数学归纳法成立。}

设 \texttt{P(n)} 是关于自然数的命题，假如
\begin{itemize}
\item \texttt{P(0)} 为真
\item 如果 \texttt{P(n)} ，那么 \texttt{P(n++)} 也为真
\end{itemize}

则 \texttt{P} 对于所有自然数都成立。
\end{frame}

\begin{frame}[fragile,label={sec:org0c109e5}]{Peano Encoding 一些其他公理（三-二）}
 这是为了排除 N = \{0, 0.5, 1, 1.5, \ldots{}\} 的情况。

证明，设 P(n) 为: \texttt{n} 是 \texttt{0} 或者某个自然数的后继

\begin{itemize}
\item \texttt{P(0)} 为真
\item 如果 \texttt{P(n)} 是真的，即，n 是 \texttt{0} 或者某个数后继
那么 \texttt{P(n++)} 也是真的（ \texttt{n++} 为 \texttt{n} 的后继）
\end{itemize}

从而得出所有自然数都是 \texttt{0} ，或者某个数后继
\end{frame}

\begin{frame}[label={sec:org67b8f1d}]{加法定义}
\begin{itemize}
\item 0 + b = b
\item Succ(a) + b = a + Succ(b)
\end{itemize}
\end{frame}

\begin{frame}[label={sec:org2cf3f72}]{加法定义图解}
\begin{center}
\includegraphics[width=.9\linewidth]{images/add-def.pdf}
\end{center}
\end{frame}


\begin{frame}[fragile,label={sec:orgcded4e1}]{Typelevel Encoding}
 \begin{minted}[]{scala}
trait Sum[A <: Nat, B <: Nat] {
  type Out <: Nat
}
object Sum {
  type Aux[A <: Nat, B <: Nat, C <: Nat] = Sum[A, B] { type Out = C }
  // 对应第一个定义
  implicit def sum1[B <: Nat]: Aux[_0, B, B] =
    new Sum[_0, B] { type Out = B }
  // 对应第二个定义
  implicit def sum2[A <: Nat, B <: Nat, C <: Nat]
    (implicit sum : Sum.Aux[A, Succ[B], C]): Aux[Succ[A], B, C] =
    new Sum[Succ[A], B] { type Out = C }
}
\end{minted}
\end{frame}

\begin{frame}[fragile,label={sec:org8663a33}]{简单应用}
 \begin{minted}[]{scala}
type _1 = Succ[_0]
type _2 = Succ[_1]
type _3 = Succ[_2]

def check[A <: Nat, B <: Nat](implicit sum: Sum.Aux[A, B, _3]) = {}

check[_0, _3]
check[_1, _2]
check[_2, _1]
check[_3, _0]
check[_1， _1] // 编译错误
\end{minted}
\end{frame}

\begin{frame}[fragile,label={sec:orgfc975b5}]{HList}
 \begin{itemize}
\item List：相同类型元素的列表
\item HList：不同类型元素的列表
\end{itemize}

\begin{minted}[]{scala}
sealed trait HList
final case class ::[+H, +T <: HList](head : H, tail : T) extends HList
sealed trait HNil extends HList {
  def ::[H](h: H): H :: HNil = new ::(h, this)
}
\end{minted}
\end{frame}

\begin{frame}[fragile,label={sec:orga6799a9}]{类型安全的 HList 操作}
 \alert{如何获取 HList 的第 N 个元素并且不丢失类型?}

\begin{minted}[]{scala}
trait At[L <: HList, N <: Nat] {
  type Out
  def apply(l: L): Out
}
object At {
  type Aux[L <: HList, N <: Nat, O] = At[L, N] {type Out = O}
}
implicit class HListOps[L <: HList](l: L) {
    def at(n: Nat)(implicit at: At[L, n.N]): at.Out =
      at.apply(l)
}
\end{minted}
\end{frame}

\begin{frame}[fragile,label={sec:org2457725}]{At 的推导}
 \begin{minted}[]{scala}
At[H :: T, _0] = H
At[H :: T, Succ[N]] = At[T, N]
\end{minted}
\end{frame}

\begin{frame}[fragile,label={sec:org33f7495}]{对应 Scala 代码}
 \begin{minted}[]{scala}
implicit def atZero[H, T <: HList] = new At[H :: L, _0] {
  type Out = H
  def apply(l: H :: T) = l.head
}
implicit def atN[H, T <: HList, N <: Nat]
  (implicit att: At[L, N]): At[H :: L, Succ[N]] =

  new At[H :: L, Succ[N]]{
    type Out = att.Out
    def apply(h: H :: T) = att.apply(h.tail)
}
\end{minted}
\end{frame}

\begin{frame}[fragile,label={sec:orgf0cca27}]{Generic}
 \begin{minted}[]{scala}
trait Generic[T] extends Serializable {
  def to(t : T) : Repr
  def from(r : Repr) : T
}
\end{minted}
\end{frame}

\begin{frame}[label={sec:org826a0f3}]{Product 和 HList}
\begin{center}
\includegraphics[width=.9\linewidth]{images/generic.pdf}
\end{center}
\end{frame}

\begin{frame}[fragile,label={sec:org08d2163}]{Show}
 \begin{minted}[]{scala}
trait Show[A] {
  def show(a: A): String
}
\end{minted}
\end{frame}

\begin{frame}[fragile,label={sec:org6436741}]{HList 实例}
 \begin{minted}[]{scala}
implicit val hnilShow: Show[HNil] = new Show[HNil] {
  def show(a: HNil) = ""
}
implicit def hlistShow[H, T <: HList](
  implicit hs: Show[H], ts: Show[T]
): Show[H :: T] = new Show[H :: T]{
  def show(a: H :: T) = hs.show(a.head) + "," + ts.show(a.tail)
}
\end{minted}
\end{frame}

\begin{frame}[fragile,label={sec:orga42d2a6}]{Case class 实例}
 \begin{minted}[]{scala}
implicit def caseClassShow[A, R <: HList](
 implicit    gen: Generic.Aux[A, R], hlistShow: Show[R]
): Show[A] = new Show[A] {
  def show(a: A) = hlistShow.show(gen.to(a))
}
\end{minted}
\end{frame}

\begin{frame}[fragile,label={sec:org1579345}]{LabelledGeneric}
 \alert{Generic 带上字段(名)信息}

\begin{minted}[]{scala}
case class Foo(i: Int)
LabelledGeneric[Foo]
// Repr = FieldType[Int, KeyTag[i'.narrow, Int]] :: HNil
\end{minted}
\end{frame}

\begin{frame}[fragile,label={sec:org06abb0a}]{Singleton type}
 \begin{minted}[]{scala}
Symbol("i").narrow //Symbol with shapeless.tag.Tagged[String("i")] = 'i
\end{minted}
\end{frame}

\begin{frame}[fragile,label={sec:orgb454f48}]{By-Name Implicit}
 \begin{minted}[]{scala}
case class Foo(
  i: Int,
  arr: Seq[Foo]
)
\end{minted}
\end{frame}

\begin{frame}[label={sec:org9f77e0f}]{Thx}
\url{https://github.com/jilen}

\url{https://scala.cool}
\end{frame}
\end{document}